\selectlanguage{portuguese}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%As the title indicates, this is a textbook on formal logic.  Formal logic concerns the study of a certain kind of language which, 
%like any language, can serve to express states of affairs.  It is a formal language, i.e., its expressions (such as sentences) are 
%defined formally.  This makes it a very useful language for being very precise about the states of %affairs its sentences describe. 
%In particular, in formal logic it is impossible to be ambiguous. The study of these languages centres on the relationship of entailment
%between sentences, i.e., which sentences follow from which other sentences.  Entailment is central because by understanding it better 
%we can tell when some states of affairs must obtain provided some other states of affairs obtain.  But entailment is not the only 
%important notion. We will also consider the relationship of being satisfiable, i.e., of not being mutually contradictory.  
%These notions can be defined semantically, using precise definitions of entailment based on interpretations of the 
%language---or proof-theoretically, using formal systems of deduction.

%Formal logic is of course a central sub-discipline of philosophy, where the logical relationship of assumptions to conclusions reached
%from them is important.  Philosophers investigate the consequences of definitions and assumptions and evaluate these definitions and 
%assumptions on the basis of their consequences. It is also important in mathematics and computer science. In mathematics, formal 
%languages are used to describe not ``everyday'' states of affairs, but mathematical states of affairs. Mathematicians are also 
%interested in the consequences of definitions and assumptions, and for them it is equally important to establish these consequences 
%(which they call ``theorems'') using completely precise and rigorous methods. Formal logic provides such methods.  In computer science,
%formal logic is applied to describe the state and behaviours of computational systems, e.g., circuits, programs, databases, etc. 
%Methods of formal logic can likewise be used to establish consequences of such descriptions, such as whether a circuit is error-free,
%whether a program does what it's intended to do, whether a database is consistent or if something is true of the data in it.

%The book is divided into nine parts. Part~\ref{ch.intro} introduces the topic and notions of logic in an informal way, without 
%introducing a formal language yet.  Parts \ref{ch.TFL}--\ref{ch.NDTFL} concern truth-functional languages. In it, sentences are formed 
%from basic sentences using a number of connectives (`or', `and', `not', `if \dots then') which just combine sentences into more 
%complicated ones.  We discuss logical notions such as entailment in two ways : semantically, using the method of truth tables 
%(in Part~\ref{ch.TruthTables}) and proof-theoretically, using a system of formal derivations (in Part~\ref{ch.NDTFL}). 
%Parts \ref{ch.FOL}--\ref{ch.NDFOL} deal with a more complicated language, that of first-order logic. It includes, in addition to the 
%connectives of truth-functional logic, also names, predicates, identity, and the so-called quantifiers.  These additional elements of 
%the language make it much more expressive than the truth-functional language, and we'll spend a fair amount of time investigating just 
%how much one can express in it.  Again, logical notions for the language of first-order logic are defined semantically, using 
%interpretations, and proof-theoretically, using a more complex version of the formal derivation system introduced in 
%Part~\ref{ch.NDTFL}. Part~\ref{ch.ML} discusses the extension of TFL by non-truth-functional operators for possibility and necessity:
%modal logic. Part~\ref{ch.normalform} covers two advanced topics: that of conjunctive and disjunctive normal forms and the expressive 
%adequacy of the truth-functional connectives, and the soundness of natural deduction for TFL.

%In the appendices you'll find a discussion of alternative notations for the languages we discuss in this text, of alternative 
%derivation systems, and a quick reference listing most of the important rules and definitions. The central terms are listed in a 
%glossary at the very end.

%This book is based on a text originally written by P.~D. Magnus in the version revised and expanded by Tim Button. It also includes 
%some material (mainly exercises) by J.~Robert Loftis. The material in Part~\ref{ch.ML} is based on notes by Robert Trueman, and the 
%material in Part~\ref{ch.normalform} on two chapters from Tim Button's open text \emph{Metatheory}. Aaron Thomas-Bolduc and Richard Zach
%have combined elements of these texts into the present version, changed some of the terminology and examples, rewritten some sections, 
%and added material of their own.  The resulting text is licensed under a Creative Commons Attribution 4.0 license.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\chapter{Prefácio}
Como o título indica, isto é um manual sobre lógica formal. Lógica formal ocupa-se com o estudo de um certo tipo de linguagem que, 
semelhante a qualquer linguagem, pode expressar estados de coisas [\textit{states of affairs}]. É uma linguagem formal, ou seja, 
as suas expressões (tais como sentenças) são definidas formalmente. Isto torna-a uma linguagem muito útil, pois ela é bastante 
precisa sobre os estados de coisas que suas sentenças descrevem. Em particular, na lógica formal é impossível ser ambíguo. O estudo 
dessas linguagens centram-se sobre as relações de acarretamento [\textit{entailment}] entre sentenças, isto é, quais sentenças se seguem
de quais outras sentenças. Acarretamento [\textit{entailment}] é central, porque, ao entendê-lo melhor, podemos dizer quando alguns 
estados de coisas [\textit{states of affairs}] devem ocorrer, uma vez que outros estados de coisas [\textit{states of affairs}] ocorrem.
Mas acarretamento [\textit{entailment}] não é a única noção importante. Também consideraremos a relação de ser satisfatível, ou seja, de
não ser mutuamente contraditório. Essas noções podem ser definidas semanticamente, usando definições precisas de acarretamento baseadas
em interpretações da linguagem --- ou prova-teoricamente [\textit{proof-theoretically}], usando sistemas formais de dedução.

Lógica formal é, obviamente, uma sub-disciplina central da filosofia, onde a relação lógica das suposições [\textit{assumptions}] às 
conclusões alcançadas a partir daquelas [as suposições] é importante. Filósofos investigam as consequências de definições e suposições
e avaliam estas definições e suposições em base das suas consequências. Ela também é importante na matemática e ciência da computação.
Na matemática, linguagens formais são usadas para descrever não estados de coisas ``cotidianos'', mas sim estados de coisas matemáticos.
Matemáticos também estão interessados nas consequências de definições e suposições e para eles é igualmente importante estabelecer essas
consequências (que eles chamam ``teoremas''), usando métodos completamente precisos e rigorosos. Lógica formal fornece tais métodos. Na
ciência da computação, lógica formal é aplicada para descrever o estado e os procedimentos de sistemas computacionais, por exemplo, 
circuitos, programas, base de dados etc. Métodos da lógica formal podem ser similarmente usados para estabelecer consequências de tais
descrições, tais como se um circuito é livre de erro, se um programa faz o que é pretendido qu ele faça, se uma base de dados é 
consistente ou se algo é verdadeiro dos dados nela.

O livro está dividido em nove partes. A Parte~\ref{ch.intro} introduz o tópico e as noções de lógica de maneira informal, sem introduzir
uma linguagem formal ainda. As Partes \ref{ch.TFL}--\ref{ch.NDTFL} ocupam-se com linguagens veri-funcionais. Nelas sentenças são 
formadas a partir de sentenças básicas, usando-se alguns conectivos (`ou', `e', `não', `se \ldots, então') que combinam justamente 
sentenças [formando] sentenças mais complicadas. Discutimos noções lógicas tais como acarretamento [\textit{entailment}] em duas formas:
semanticamente, usando o método de tabelas de verdade (na Parte~\ref{ch.TruthTables}) e prova-teoricamente, usando um sistema de 
derivações formais (na Parte~\ref{ch.NDTFL}). As Partes \ref{ch.FOL}--\ref{ch.NDFOL} lidam com uma linguagem mais complicada, a da 
lógica de primeira ordem. Ela inclui, além dos conectivos da lógica veri-funcional, também nomes, predicados, identidade e os então 
chamados quantificadores. Estes elementos adicionais da linguagem a tornam muita mais expressiva do que a linguagem veri-funcional e 
passaremos uma grande quantidade de tempo investigando justamente o quanto se pode expressar nela. Novamente, noções lógicas para 
linguagem da lógica de primeira ordem são definidas semanticamente, usando-se interpretações, e prova-teoricamente, usando-se uma 
versão mais complexa do sistema de derivação formal introduzido na Parte~\ref{ch.NDTFL}.  Parte~\ref{ch.ML} discute a extensão da TFL
por meio de operadores não-veri-funcionais para possibilidade e necessidade: lógica modal. Parte~\ref{ch.normalform} cobre dois tópicos 
avançados: o primeiro diz respeito às formas normais conjuntivas e disjuntivas e à adequação expressiva dos conectivos veri-funcionais;
o segundo diz respeito à corretude [\textit{soundness}] da dedução natural para TFL.

Nos apêndices, você encontrará uma discussão de notações alternativas para as linguagens que discutimos neste texto, discussão de 
sistemas alternatrivos de derivação e uma rápida referência que lista as regras e definições mais importantes. Os termos centrais são
listados em um glossário no fim.

Este livro é baseado em um texto que foi originalmente escrito por P.~D. Magnus na versão revisada e expandida por Tim Button. Ele 
também inclui algum material de J.~Robert Loftis. O material na Parte~\ref{ch.ML} é baseada em notas de Robert Trueman e o material na
Parte~\ref{ch.normalform} é baseado em dois capítulos do texto aberto \emph{Metatheory} de Tim Button. Aaron Thomas-Bolduc e Richard
Zach combinaram elementos destes textos na presente versão, mudaram algumas terminologia e alguns exemplos, reescreveram algumas seções
e adicionaram material próprio. O texto resultante é licenciado sob uma licença Creative Commons Attribution 4.0.

%   
